A recent heuristic technique that has been used to reason with programs manipulating datastructures, both functional and imperative programs, involves unfolding recursive definitions followed by quantifier-free SMT reasoning. This tutorial will go into certain theoretical foundations that have recently emerged arguing that these heuristics, far from being whimsical heuristics, are complete for certain abstractions of the verification problem. These elucidate the role of user help required in tools that employ these heuristics and open up general new techniques for quantified first-order logic reasoning over combined theories using SMT solvers. The tutorial will describe this new technique, summarize the associated completeness results, and the applications of the technique to verification of programs that manipulate datastructures.